0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 383 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 90 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 PiDPToQDPProof (⇒, 0 ms)
↳16 QDP
↳17 QDPSizeChangeProof (⇔, 0 ms)
↳18 YES
TRANSPOSED_IN_GA(.(X1, X2), .(X3, X4)) → U5_GA(X1, X2, X3, X4, pB_in_gaaaag(X1, X3, X4, X5, X6, X2))
TRANSPOSED_IN_GA(.(X1, X2), .(X3, X4)) → PB_IN_GAAAAG(X1, X3, X4, X5, X6, X2)
PB_IN_GAAAAG(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), .(X1, X10), .(.(X2, X11), .(.(X3, X12), .(.(X4, X13), .(.(X5, X14), .(.(X6, X15), .(.(X7, X16), .(.(X8, X17), X18))))))), .(X10, .(X11, .(X12, .(X13, .(X14, .(X15, .(X16, .(X17, X19)))))))), X20, X21) → U2_GAAAAG(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, row2colA_in_gaaga(X9, X18, X19, .([], .([], .([], .([], .([], .([], .([], []))))))), X20))
PB_IN_GAAAAG(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), .(X1, X10), .(.(X2, X11), .(.(X3, X12), .(.(X4, X13), .(.(X5, X14), .(.(X6, X15), .(.(X7, X16), .(.(X8, X17), X18))))))), .(X10, .(X11, .(X12, .(X13, .(X14, .(X15, .(X16, .(X17, X19)))))))), X20, X21) → ROW2COLA_IN_GAAGA(X9, X18, X19, .([], .([], .([], .([], .([], .([], .([], []))))))), X20)
ROW2COLA_IN_GAAGA(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), X6, X7) → U1_GAAGA(X1, X2, X3, X4, X5, X6, X7, row2colA_in_gaaga(X2, X4, X5, .([], X6), X7))
ROW2COLA_IN_GAAGA(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), X6, X7) → ROW2COLA_IN_GAAGA(X2, X4, X5, .([], X6), X7)
PB_IN_GAAAAG(X1, X2, X3, .(X4, X5), X6, .(X7, X8)) → U3_GAAAAG(X1, X2, X3, X4, X5, X6, X7, X8, row2colcC_in_gaaaa(X1, X2, X3, .(X4, X5), X6))
U3_GAAAAG(X1, X2, X3, X4, X5, X6, X7, X8, row2colcC_out_gaaaa(X1, X2, X3, .(X4, X5), X6)) → U4_GAAAAG(X1, X2, X3, X4, X5, X6, X7, X8, pB_in_gaaaag(X7, X4, X5, X9, X10, X8))
U3_GAAAAG(X1, X2, X3, X4, X5, X6, X7, X8, row2colcC_out_gaaaa(X1, X2, X3, .(X4, X5), X6)) → PB_IN_GAAAAG(X7, X4, X5, X9, X10, X8)
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), .(X1, X10), .(.(X2, X11), .(.(X3, X12), .(.(X4, X13), .(.(X5, X14), .(.(X6, X15), .(.(X7, X16), .(.(X8, X17), X18))))))), .(X10, .(X11, .(X12, .(X13, .(X14, .(X15, .(X16, .(X17, X19)))))))), X20) → U11_gaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, row2colcA_in_gaaga(X9, X18, X19, .([], .([], .([], .([], .([], .([], .([], []))))))), X20))
row2colcA_in_gaaga(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), X6, X7) → U7_gaaga(X1, X2, X3, X4, X5, X6, X7, row2colcA_in_gaaga(X2, X4, X5, .([], X6), X7))
row2colcA_in_gaaga([], [], [], X1, .([], X1)) → row2colcA_out_gaaga([], [], [], X1, .([], X1))
U7_gaaga(X1, X2, X3, X4, X5, X6, X7, row2colcA_out_gaaga(X2, X4, X5, .([], X6), X7)) → row2colcA_out_gaaga(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), X6, X7)
U11_gaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, row2colcA_out_gaaga(X9, X18, X19, .([], .([], .([], .([], .([], .([], .([], []))))))), X20)) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), .(X1, X10), .(.(X2, X11), .(.(X3, X12), .(.(X4, X13), .(.(X5, X14), .(.(X6, X15), .(.(X7, X16), .(.(X8, X17), X18))))))), .(X10, .(X11, .(X12, .(X13, .(X14, .(X15, .(X16, .(X17, X19)))))))), X20)
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), .(X1, X8), .(.(X2, X9), .(.(X3, X10), .(.(X4, X11), .(.(X5, X12), .(.(X6, X13), .(.(X7, X14), [])))))), .(X8, .(X9, .(X10, .(X11, .(X12, .(X13, .(X14, []))))))), .([], .([], .([], .([], .([], .([], .([], [])))))))) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), .(X1, X8), .(.(X2, X9), .(.(X3, X10), .(.(X4, X11), .(.(X5, X12), .(.(X6, X13), .(.(X7, X14), [])))))), .(X8, .(X9, .(X10, .(X11, .(X12, .(X13, .(X14, []))))))), .([], .([], .([], .([], .([], .([], .([], []))))))))
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), .(X1, X7), .(.(X2, X8), .(.(X3, X9), .(.(X4, X10), .(.(X5, X11), .(.(X6, X12), []))))), .(X7, .(X8, .(X9, .(X10, .(X11, .(X12, [])))))), .([], .([], .([], .([], .([], .([], []))))))) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), .(X1, X7), .(.(X2, X8), .(.(X3, X9), .(.(X4, X10), .(.(X5, X11), .(.(X6, X12), []))))), .(X7, .(X8, .(X9, .(X10, .(X11, .(X12, [])))))), .([], .([], .([], .([], .([], .([], [])))))))
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), .(X1, X6), .(.(X2, X7), .(.(X3, X8), .(.(X4, X9), .(.(X5, X10), [])))), .(X6, .(X7, .(X8, .(X9, .(X10, []))))), .([], .([], .([], .([], .([], [])))))) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), .(X1, X6), .(.(X2, X7), .(.(X3, X8), .(.(X4, X9), .(.(X5, X10), [])))), .(X6, .(X7, .(X8, .(X9, .(X10, []))))), .([], .([], .([], .([], .([], []))))))
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, .(X4, [])))), .(X1, X5), .(.(X2, X6), .(.(X3, X7), .(.(X4, X8), []))), .(X5, .(X6, .(X7, .(X8, [])))), .([], .([], .([], .([], []))))) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, .(X4, [])))), .(X1, X5), .(.(X2, X6), .(.(X3, X7), .(.(X4, X8), []))), .(X5, .(X6, .(X7, .(X8, [])))), .([], .([], .([], .([], [])))))
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, []))), .(X1, X4), .(.(X2, X5), .(.(X3, X6), [])), .(X4, .(X5, .(X6, []))), .([], .([], .([], [])))) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, []))), .(X1, X4), .(.(X2, X5), .(.(X3, X6), [])), .(X4, .(X5, .(X6, []))), .([], .([], .([], []))))
row2colcC_in_gaaaa(.(X1, .(X2, [])), .(X1, X3), .(.(X2, X4), []), .(X3, .(X4, [])), .([], .([], []))) → row2colcC_out_gaaaa(.(X1, .(X2, [])), .(X1, X3), .(.(X2, X4), []), .(X3, .(X4, [])), .([], .([], [])))
row2colcC_in_gaaaa(.(X1, []), .(X1, X2), [], .(X2, []), .([], [])) → row2colcC_out_gaaaa(.(X1, []), .(X1, X2), [], .(X2, []), .([], []))
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
TRANSPOSED_IN_GA(.(X1, X2), .(X3, X4)) → U5_GA(X1, X2, X3, X4, pB_in_gaaaag(X1, X3, X4, X5, X6, X2))
TRANSPOSED_IN_GA(.(X1, X2), .(X3, X4)) → PB_IN_GAAAAG(X1, X3, X4, X5, X6, X2)
PB_IN_GAAAAG(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), .(X1, X10), .(.(X2, X11), .(.(X3, X12), .(.(X4, X13), .(.(X5, X14), .(.(X6, X15), .(.(X7, X16), .(.(X8, X17), X18))))))), .(X10, .(X11, .(X12, .(X13, .(X14, .(X15, .(X16, .(X17, X19)))))))), X20, X21) → U2_GAAAAG(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, row2colA_in_gaaga(X9, X18, X19, .([], .([], .([], .([], .([], .([], .([], []))))))), X20))
PB_IN_GAAAAG(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), .(X1, X10), .(.(X2, X11), .(.(X3, X12), .(.(X4, X13), .(.(X5, X14), .(.(X6, X15), .(.(X7, X16), .(.(X8, X17), X18))))))), .(X10, .(X11, .(X12, .(X13, .(X14, .(X15, .(X16, .(X17, X19)))))))), X20, X21) → ROW2COLA_IN_GAAGA(X9, X18, X19, .([], .([], .([], .([], .([], .([], .([], []))))))), X20)
ROW2COLA_IN_GAAGA(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), X6, X7) → U1_GAAGA(X1, X2, X3, X4, X5, X6, X7, row2colA_in_gaaga(X2, X4, X5, .([], X6), X7))
ROW2COLA_IN_GAAGA(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), X6, X7) → ROW2COLA_IN_GAAGA(X2, X4, X5, .([], X6), X7)
PB_IN_GAAAAG(X1, X2, X3, .(X4, X5), X6, .(X7, X8)) → U3_GAAAAG(X1, X2, X3, X4, X5, X6, X7, X8, row2colcC_in_gaaaa(X1, X2, X3, .(X4, X5), X6))
U3_GAAAAG(X1, X2, X3, X4, X5, X6, X7, X8, row2colcC_out_gaaaa(X1, X2, X3, .(X4, X5), X6)) → U4_GAAAAG(X1, X2, X3, X4, X5, X6, X7, X8, pB_in_gaaaag(X7, X4, X5, X9, X10, X8))
U3_GAAAAG(X1, X2, X3, X4, X5, X6, X7, X8, row2colcC_out_gaaaa(X1, X2, X3, .(X4, X5), X6)) → PB_IN_GAAAAG(X7, X4, X5, X9, X10, X8)
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), .(X1, X10), .(.(X2, X11), .(.(X3, X12), .(.(X4, X13), .(.(X5, X14), .(.(X6, X15), .(.(X7, X16), .(.(X8, X17), X18))))))), .(X10, .(X11, .(X12, .(X13, .(X14, .(X15, .(X16, .(X17, X19)))))))), X20) → U11_gaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, row2colcA_in_gaaga(X9, X18, X19, .([], .([], .([], .([], .([], .([], .([], []))))))), X20))
row2colcA_in_gaaga(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), X6, X7) → U7_gaaga(X1, X2, X3, X4, X5, X6, X7, row2colcA_in_gaaga(X2, X4, X5, .([], X6), X7))
row2colcA_in_gaaga([], [], [], X1, .([], X1)) → row2colcA_out_gaaga([], [], [], X1, .([], X1))
U7_gaaga(X1, X2, X3, X4, X5, X6, X7, row2colcA_out_gaaga(X2, X4, X5, .([], X6), X7)) → row2colcA_out_gaaga(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), X6, X7)
U11_gaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, row2colcA_out_gaaga(X9, X18, X19, .([], .([], .([], .([], .([], .([], .([], []))))))), X20)) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), .(X1, X10), .(.(X2, X11), .(.(X3, X12), .(.(X4, X13), .(.(X5, X14), .(.(X6, X15), .(.(X7, X16), .(.(X8, X17), X18))))))), .(X10, .(X11, .(X12, .(X13, .(X14, .(X15, .(X16, .(X17, X19)))))))), X20)
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), .(X1, X8), .(.(X2, X9), .(.(X3, X10), .(.(X4, X11), .(.(X5, X12), .(.(X6, X13), .(.(X7, X14), [])))))), .(X8, .(X9, .(X10, .(X11, .(X12, .(X13, .(X14, []))))))), .([], .([], .([], .([], .([], .([], .([], [])))))))) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), .(X1, X8), .(.(X2, X9), .(.(X3, X10), .(.(X4, X11), .(.(X5, X12), .(.(X6, X13), .(.(X7, X14), [])))))), .(X8, .(X9, .(X10, .(X11, .(X12, .(X13, .(X14, []))))))), .([], .([], .([], .([], .([], .([], .([], []))))))))
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), .(X1, X7), .(.(X2, X8), .(.(X3, X9), .(.(X4, X10), .(.(X5, X11), .(.(X6, X12), []))))), .(X7, .(X8, .(X9, .(X10, .(X11, .(X12, [])))))), .([], .([], .([], .([], .([], .([], []))))))) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), .(X1, X7), .(.(X2, X8), .(.(X3, X9), .(.(X4, X10), .(.(X5, X11), .(.(X6, X12), []))))), .(X7, .(X8, .(X9, .(X10, .(X11, .(X12, [])))))), .([], .([], .([], .([], .([], .([], [])))))))
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), .(X1, X6), .(.(X2, X7), .(.(X3, X8), .(.(X4, X9), .(.(X5, X10), [])))), .(X6, .(X7, .(X8, .(X9, .(X10, []))))), .([], .([], .([], .([], .([], [])))))) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), .(X1, X6), .(.(X2, X7), .(.(X3, X8), .(.(X4, X9), .(.(X5, X10), [])))), .(X6, .(X7, .(X8, .(X9, .(X10, []))))), .([], .([], .([], .([], .([], []))))))
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, .(X4, [])))), .(X1, X5), .(.(X2, X6), .(.(X3, X7), .(.(X4, X8), []))), .(X5, .(X6, .(X7, .(X8, [])))), .([], .([], .([], .([], []))))) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, .(X4, [])))), .(X1, X5), .(.(X2, X6), .(.(X3, X7), .(.(X4, X8), []))), .(X5, .(X6, .(X7, .(X8, [])))), .([], .([], .([], .([], [])))))
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, []))), .(X1, X4), .(.(X2, X5), .(.(X3, X6), [])), .(X4, .(X5, .(X6, []))), .([], .([], .([], [])))) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, []))), .(X1, X4), .(.(X2, X5), .(.(X3, X6), [])), .(X4, .(X5, .(X6, []))), .([], .([], .([], []))))
row2colcC_in_gaaaa(.(X1, .(X2, [])), .(X1, X3), .(.(X2, X4), []), .(X3, .(X4, [])), .([], .([], []))) → row2colcC_out_gaaaa(.(X1, .(X2, [])), .(X1, X3), .(.(X2, X4), []), .(X3, .(X4, [])), .([], .([], [])))
row2colcC_in_gaaaa(.(X1, []), .(X1, X2), [], .(X2, []), .([], [])) → row2colcC_out_gaaaa(.(X1, []), .(X1, X2), [], .(X2, []), .([], []))
ROW2COLA_IN_GAAGA(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), X6, X7) → ROW2COLA_IN_GAAGA(X2, X4, X5, .([], X6), X7)
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), .(X1, X10), .(.(X2, X11), .(.(X3, X12), .(.(X4, X13), .(.(X5, X14), .(.(X6, X15), .(.(X7, X16), .(.(X8, X17), X18))))))), .(X10, .(X11, .(X12, .(X13, .(X14, .(X15, .(X16, .(X17, X19)))))))), X20) → U11_gaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, row2colcA_in_gaaga(X9, X18, X19, .([], .([], .([], .([], .([], .([], .([], []))))))), X20))
row2colcA_in_gaaga(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), X6, X7) → U7_gaaga(X1, X2, X3, X4, X5, X6, X7, row2colcA_in_gaaga(X2, X4, X5, .([], X6), X7))
row2colcA_in_gaaga([], [], [], X1, .([], X1)) → row2colcA_out_gaaga([], [], [], X1, .([], X1))
U7_gaaga(X1, X2, X3, X4, X5, X6, X7, row2colcA_out_gaaga(X2, X4, X5, .([], X6), X7)) → row2colcA_out_gaaga(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), X6, X7)
U11_gaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, row2colcA_out_gaaga(X9, X18, X19, .([], .([], .([], .([], .([], .([], .([], []))))))), X20)) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), .(X1, X10), .(.(X2, X11), .(.(X3, X12), .(.(X4, X13), .(.(X5, X14), .(.(X6, X15), .(.(X7, X16), .(.(X8, X17), X18))))))), .(X10, .(X11, .(X12, .(X13, .(X14, .(X15, .(X16, .(X17, X19)))))))), X20)
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), .(X1, X8), .(.(X2, X9), .(.(X3, X10), .(.(X4, X11), .(.(X5, X12), .(.(X6, X13), .(.(X7, X14), [])))))), .(X8, .(X9, .(X10, .(X11, .(X12, .(X13, .(X14, []))))))), .([], .([], .([], .([], .([], .([], .([], [])))))))) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), .(X1, X8), .(.(X2, X9), .(.(X3, X10), .(.(X4, X11), .(.(X5, X12), .(.(X6, X13), .(.(X7, X14), [])))))), .(X8, .(X9, .(X10, .(X11, .(X12, .(X13, .(X14, []))))))), .([], .([], .([], .([], .([], .([], .([], []))))))))
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), .(X1, X7), .(.(X2, X8), .(.(X3, X9), .(.(X4, X10), .(.(X5, X11), .(.(X6, X12), []))))), .(X7, .(X8, .(X9, .(X10, .(X11, .(X12, [])))))), .([], .([], .([], .([], .([], .([], []))))))) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), .(X1, X7), .(.(X2, X8), .(.(X3, X9), .(.(X4, X10), .(.(X5, X11), .(.(X6, X12), []))))), .(X7, .(X8, .(X9, .(X10, .(X11, .(X12, [])))))), .([], .([], .([], .([], .([], .([], [])))))))
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), .(X1, X6), .(.(X2, X7), .(.(X3, X8), .(.(X4, X9), .(.(X5, X10), [])))), .(X6, .(X7, .(X8, .(X9, .(X10, []))))), .([], .([], .([], .([], .([], [])))))) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), .(X1, X6), .(.(X2, X7), .(.(X3, X8), .(.(X4, X9), .(.(X5, X10), [])))), .(X6, .(X7, .(X8, .(X9, .(X10, []))))), .([], .([], .([], .([], .([], []))))))
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, .(X4, [])))), .(X1, X5), .(.(X2, X6), .(.(X3, X7), .(.(X4, X8), []))), .(X5, .(X6, .(X7, .(X8, [])))), .([], .([], .([], .([], []))))) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, .(X4, [])))), .(X1, X5), .(.(X2, X6), .(.(X3, X7), .(.(X4, X8), []))), .(X5, .(X6, .(X7, .(X8, [])))), .([], .([], .([], .([], [])))))
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, []))), .(X1, X4), .(.(X2, X5), .(.(X3, X6), [])), .(X4, .(X5, .(X6, []))), .([], .([], .([], [])))) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, []))), .(X1, X4), .(.(X2, X5), .(.(X3, X6), [])), .(X4, .(X5, .(X6, []))), .([], .([], .([], []))))
row2colcC_in_gaaaa(.(X1, .(X2, [])), .(X1, X3), .(.(X2, X4), []), .(X3, .(X4, [])), .([], .([], []))) → row2colcC_out_gaaaa(.(X1, .(X2, [])), .(X1, X3), .(.(X2, X4), []), .(X3, .(X4, [])), .([], .([], [])))
row2colcC_in_gaaaa(.(X1, []), .(X1, X2), [], .(X2, []), .([], [])) → row2colcC_out_gaaaa(.(X1, []), .(X1, X2), [], .(X2, []), .([], []))
ROW2COLA_IN_GAAGA(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), X6, X7) → ROW2COLA_IN_GAAGA(X2, X4, X5, .([], X6), X7)
ROW2COLA_IN_GAAGA(.(X1, X2), X6) → ROW2COLA_IN_GAAGA(X2, .([], X6))
From the DPs we obtained the following set of size-change graphs:
PB_IN_GAAAAG(X1, X2, X3, .(X4, X5), X6, .(X7, X8)) → U3_GAAAAG(X1, X2, X3, X4, X5, X6, X7, X8, row2colcC_in_gaaaa(X1, X2, X3, .(X4, X5), X6))
U3_GAAAAG(X1, X2, X3, X4, X5, X6, X7, X8, row2colcC_out_gaaaa(X1, X2, X3, .(X4, X5), X6)) → PB_IN_GAAAAG(X7, X4, X5, X9, X10, X8)
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), .(X1, X10), .(.(X2, X11), .(.(X3, X12), .(.(X4, X13), .(.(X5, X14), .(.(X6, X15), .(.(X7, X16), .(.(X8, X17), X18))))))), .(X10, .(X11, .(X12, .(X13, .(X14, .(X15, .(X16, .(X17, X19)))))))), X20) → U11_gaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, row2colcA_in_gaaga(X9, X18, X19, .([], .([], .([], .([], .([], .([], .([], []))))))), X20))
row2colcA_in_gaaga(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), X6, X7) → U7_gaaga(X1, X2, X3, X4, X5, X6, X7, row2colcA_in_gaaga(X2, X4, X5, .([], X6), X7))
row2colcA_in_gaaga([], [], [], X1, .([], X1)) → row2colcA_out_gaaga([], [], [], X1, .([], X1))
U7_gaaga(X1, X2, X3, X4, X5, X6, X7, row2colcA_out_gaaga(X2, X4, X5, .([], X6), X7)) → row2colcA_out_gaaga(.(X1, X2), .(.(X1, X3), X4), .(X3, X5), X6, X7)
U11_gaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, row2colcA_out_gaaga(X9, X18, X19, .([], .([], .([], .([], .([], .([], .([], []))))))), X20)) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), .(X1, X10), .(.(X2, X11), .(.(X3, X12), .(.(X4, X13), .(.(X5, X14), .(.(X6, X15), .(.(X7, X16), .(.(X8, X17), X18))))))), .(X10, .(X11, .(X12, .(X13, .(X14, .(X15, .(X16, .(X17, X19)))))))), X20)
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), .(X1, X8), .(.(X2, X9), .(.(X3, X10), .(.(X4, X11), .(.(X5, X12), .(.(X6, X13), .(.(X7, X14), [])))))), .(X8, .(X9, .(X10, .(X11, .(X12, .(X13, .(X14, []))))))), .([], .([], .([], .([], .([], .([], .([], [])))))))) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), .(X1, X8), .(.(X2, X9), .(.(X3, X10), .(.(X4, X11), .(.(X5, X12), .(.(X6, X13), .(.(X7, X14), [])))))), .(X8, .(X9, .(X10, .(X11, .(X12, .(X13, .(X14, []))))))), .([], .([], .([], .([], .([], .([], .([], []))))))))
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), .(X1, X7), .(.(X2, X8), .(.(X3, X9), .(.(X4, X10), .(.(X5, X11), .(.(X6, X12), []))))), .(X7, .(X8, .(X9, .(X10, .(X11, .(X12, [])))))), .([], .([], .([], .([], .([], .([], []))))))) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), .(X1, X7), .(.(X2, X8), .(.(X3, X9), .(.(X4, X10), .(.(X5, X11), .(.(X6, X12), []))))), .(X7, .(X8, .(X9, .(X10, .(X11, .(X12, [])))))), .([], .([], .([], .([], .([], .([], [])))))))
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), .(X1, X6), .(.(X2, X7), .(.(X3, X8), .(.(X4, X9), .(.(X5, X10), [])))), .(X6, .(X7, .(X8, .(X9, .(X10, []))))), .([], .([], .([], .([], .([], [])))))) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), .(X1, X6), .(.(X2, X7), .(.(X3, X8), .(.(X4, X9), .(.(X5, X10), [])))), .(X6, .(X7, .(X8, .(X9, .(X10, []))))), .([], .([], .([], .([], .([], []))))))
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, .(X4, [])))), .(X1, X5), .(.(X2, X6), .(.(X3, X7), .(.(X4, X8), []))), .(X5, .(X6, .(X7, .(X8, [])))), .([], .([], .([], .([], []))))) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, .(X4, [])))), .(X1, X5), .(.(X2, X6), .(.(X3, X7), .(.(X4, X8), []))), .(X5, .(X6, .(X7, .(X8, [])))), .([], .([], .([], .([], [])))))
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, []))), .(X1, X4), .(.(X2, X5), .(.(X3, X6), [])), .(X4, .(X5, .(X6, []))), .([], .([], .([], [])))) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, []))), .(X1, X4), .(.(X2, X5), .(.(X3, X6), [])), .(X4, .(X5, .(X6, []))), .([], .([], .([], []))))
row2colcC_in_gaaaa(.(X1, .(X2, [])), .(X1, X3), .(.(X2, X4), []), .(X3, .(X4, [])), .([], .([], []))) → row2colcC_out_gaaaa(.(X1, .(X2, [])), .(X1, X3), .(.(X2, X4), []), .(X3, .(X4, [])), .([], .([], [])))
row2colcC_in_gaaaa(.(X1, []), .(X1, X2), [], .(X2, []), .([], [])) → row2colcC_out_gaaaa(.(X1, []), .(X1, X2), [], .(X2, []), .([], []))
PB_IN_GAAAAG(X1, .(X7, X8)) → U3_GAAAAG(X1, X7, X8, row2colcC_in_gaaaa(X1))
U3_GAAAAG(X1, X7, X8, row2colcC_out_gaaaa(X1, X6)) → PB_IN_GAAAAG(X7, X8)
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → U11_gaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, row2colcA_in_gaaga(X9, .([], .([], .([], .([], .([], .([], .([], [])))))))))
row2colcA_in_gaaga(.(X1, X2), X6) → U7_gaaga(X1, X2, X6, row2colcA_in_gaaga(X2, .([], X6)))
row2colcA_in_gaaga([], X1) → row2colcA_out_gaaga([], X1, .([], X1))
U7_gaaga(X1, X2, X6, row2colcA_out_gaaga(X2, .([], X6), X7)) → row2colcA_out_gaaga(.(X1, X2), X6, X7)
U11_gaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, row2colcA_out_gaaga(X9, .([], .([], .([], .([], .([], .([], .([], []))))))), X20)) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X20)
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, [])))))))) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), .([], .([], .([], .([], .([], .([], .([], []))))))))
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, []))))))) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), .([], .([], .([], .([], .([], .([], [])))))))
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, [])))))) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), .([], .([], .([], .([], .([], []))))))
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, .(X4, []))))) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, .(X4, [])))), .([], .([], .([], .([], [])))))
row2colcC_in_gaaaa(.(X1, .(X2, .(X3, [])))) → row2colcC_out_gaaaa(.(X1, .(X2, .(X3, []))), .([], .([], .([], []))))
row2colcC_in_gaaaa(.(X1, .(X2, []))) → row2colcC_out_gaaaa(.(X1, .(X2, [])), .([], .([], [])))
row2colcC_in_gaaaa(.(X1, [])) → row2colcC_out_gaaaa(.(X1, []), .([], []))
row2colcC_in_gaaaa(x0)
row2colcA_in_gaaga(x0, x1)
U7_gaaga(x0, x1, x2, x3)
U11_gaaaa(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9)
From the DPs we obtained the following set of size-change graphs: